COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		In his Stanford PhD thesis (Cartwright 1977), supported
C00006 ENDMK
C⊗;
	In his Stanford PhD thesis (Cartwright 1977), supported
by this project, R.S. Cartwright proposed a way of representing
the functional equation of a Lisp program entirely within first
order logic.  Using this and some earlier results, McCarthy (1977)
showed that the Lisp and other recursive programs can be completely
characterized within first order logic by the functional equation
and a minimization axiom schema.  It had been previously thought
that such characterization required second order logic which
is much more difficult to compute with.  McCarthy further showed that
the well known proof methods of inductive assertions and subgoal
induction were expressible as axiom schemata in first order logic.
This unexpected result makes all first order metheods  of verification
and proof-checking more valuable than expected, and it also permits
postponing the expression of the full Scott fixed point theory in
first order logic.

	In the next period we plan to exploit this breakthrough
by verifying more complex programs directly within first order logic.
Because the breakthrough is very new (February 1977), it is not
possible to say how far the new methods will go and whether it will
still be necessary to develop the extensional form theory.  Most
likely, the extensional form theory will still be needed, but
we will be able to distinguish programs of simple structure that
don't require it for their verification.

	Wolfgang Polak has an indication that subgoal induction is
exactly McCarthy's minimization schema extended to relations.  If this
is true, the list of methods for inductively proving programs correct
will be greatly shortened by showing that most of the existing
methods are subcases of more general methods.  This will make it
much easier to write verifying programs, both the automatic kind and
those that use human help.

	McCarthy has investigated continuous functionals that don't
arise from simple recursive programs.  Some of them require parallel
evaluation, and the work may lead to a treatment of program
correctness that unifies parallel programs with the more usual
sequential programs.